D:dsys{i:l}. d-feasible{i:l}(D)  {i'} 

latex

Definitions	x:A. B(x), t  T, , Feasible(D), P & Q
Lemmas	Id wf, ma-feasible wf, d-m wf, IdLnk wf, subtype rel wf, ma-dout wf, lsrc wf, ma-din wf, ldst wf, finite-type wf, assert wf, ma-sends-on wf, dsys wf